(set-logic ALL)
(set-info :status sat)
(declare-datatypes ((D 0)) (((A (a Int)))))
(declare-fun x1 () D)
(declare-fun S () (Set D))
(declare-fun P (D) Bool)
(assert (set.member x1 S))
(assert (=> (set.member (A 0) S) (P x1)))
(check-sat)
